| Definitions | i <z j,   b, i  z j, nth_tl(n;as), hd(l), l[i], e loc e' , Id, state@i, State(ds), f(x)?z, with decls ds dasends on l from e include f(e) and only these for tags in tgs, p  q, Knd, False, t ...$L, A B, i  j , A, True,  T, ff, Y, tt, if b then t else f fi , ||as||, i j < k, x(s1,s2), {i..j },  x:A. B(x), Valtype(da;k),  e@i. P(e),  , {T}, SQType(T), P  Q, A c B, es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e)),   x. t(x), P   Q, t  T, P & Q, P  Q, P Q, x:A. B(x), Dec(P),  , t.2, t.1, Unit,  , x(s),  |
| Lemmas | decidable equal Id, alle-at wf, es-locl wf, es-index-zero, es-loc-sender, subtype rel self, subtype rel dep function, fpf-ap wf, fpf-trivial-subtype-top, fpf-dom wf, subtype rel transitivity, es-val wf, es-sends-iff wf, same-sender-index, es-loc-rcv, ldst wf, fpf-sub weakening, subtype-fpf-cap-void, Id sq, pi1 wf, pi2 wf, es-E wf, length nil, length wf2, select wf, btrue wf, bfalse wf, int seg wf, es-sends wf, es-Msgl wf, non neg length, es-index wf, bool sq, bool cases, member singleton, es-tag wf, l member wf, es-lnk wf, assert-es-bact, assert-eq-knd, assert of bnot, or functionality wrt iff, assert of bor, bnot thru band, true wf, squash wf, eqff to assert, not wf, bnot wf, bor wf, assert of band, eqtt to assert, iff transitivity, bool wf, eq knd wf, band wf, es-sender wf, es-rcv-kind, es-vartype wf, es-state-subtype, es-state-when wf, ifthenelse wf, length wf1, es-bact wf, es-loc-init, es-init wf, es-valtype wf, es-isrcv wf, assert wf, ecl-es-act wf, es-kind wf, es-loc wf, es-kind-rcv, Knd sq, event system wf, IdLnk wf, Id wf, fpf wf, nat wf, ecl wf, rcv wf, Kind-deq wf, Knd wf, fpf-cap wf, ma-valtype wf, decl-state wf, lsrc wf, es-decls wf, es-decls-iff |
Type, da:k:Knd fp
f:(State(ds)